Android安全加固技术

为了保护Android智能手机安全,在深入分析Android系统安全机制的基础上,提出了一个基于强制访问控制的安全加固技术.该技术首先通过修改Android内核,添加一个平台无关的强制访问框架,其次为进程、文件等系统对象添加安全属性,最后通过制定一套细粒度的强制访问规则,对应用程序实施强制访问控制.通过在模拟环境中的测...     

基于μC/OS-Ⅱ的车载操作系统设计

根据OSEK/VDX规范,以及μC/OS-Ⅱ内核的特点,分析二者的差异,通过修改μC/OS-Ⅱ内核,设计出一种符合OSEK/VDX规范的车载嵌入式操作系统.并从任务管理与调度、资源管理、警报与计数器管理、事件管理和中断管理等多方面,详细地介绍了该系统的主要设计思想.     

出具证明编译器中线性整数命题证明的自动生成

近年来,出具证明编译器作为构建高可信软件的重要途径,逐渐成为编译器理论和形式化验证的研究热点.在其理论框架中,编译器需要借助自动定理证明技术,自动地证明验证条件并生成机器可检查的证明项,因此好的自动定理证明器对出具证明编译器至关重要.本文基于Simplex算法在出具证明编译器的框架内设计并实现了一个支持线性整数命题求解的自动定理证明器,并且提出一套证明项构造方法,将其应用于自动定理证明器中可生成Coq可检查的证明.     

复杂区域节点定位算法研究

传统的无线传感器网络节点定位算法假设节点间的最短路径长度与实际几何距离之间存在函数映射关系.然而对于布设在复杂区域的无线传感器网络而言,这种函数映射关系不再成立,直接应用传统定位算法将会带来较大的定位误差.针对复杂区域中各向异性的无线传感器网络节点定位问题,提出了一种基于参考节点凸包划分的测距无关定位算法CHP.首先,...     

渐进式标记-清扫垃圾收集机制验证

垃圾收集已经成为可靠、高效程序运行平台的一个重要组成部分.渐进式垃圾收集由于在用户程序运行时并行的执行垃圾收集操作,其算法及实现则更为复杂,其可靠性也更难以得到保证.本文论述使用Hoare风格的程序验证框架形式验证渐进式标记-清扫垃圾收集机制及其写拦截器在汇编语言层次上的实现的研究工作.被验证的属性涵括了简单的类型安全到整个内存堆上的数据保持.本文所有的验证工作都实现在Coq辅助定理证明工具中,从而可以迅速的用于构造携带证明的代码包.     

基于热点区域场景的传感器网络拓扑控制算法

无线传感器网络具有应用多样性特点,文中基于热点区域场景研究其拓扑控制问题.建立了无线传感器网络拓扑控制通用模型,进行了形式化描述和定义,分析了面向热点区域场景的拓扑控制目标和需求,提出了一种融合功率控制技术和分簇控制技术的混合式拓扑控制近似算法HTCA.HTCA能区分热点区域与非热点区域,在热点区域形成树结构并进行适当的剪接,而在非热点区域形成簇结构,该混合式拓扑结构能有效地降低全局能耗.仿真实验结果表明,HTCA能获得较优的拓扑结构,有效地延长了基于热点区域场景的无线传感器网络生命期.     

CMP中基于目录的协作Cache设计方案

片上多处理器中二级Cache的设计和管理是影响其性能的关键因素之一。在私有二级Cache的基础上,提出一种基于集中式一致性目录的协作Cache设计方案,通过有效地管理片上存储资源来优化处理器的性能,从而使该协作Cache具有平均访存延迟小、Cache缺失率低、可扩展性好等优点。实验结果显示,与共享二级Cache设计相比,协作Cache可以将4核处理器的吞吐量平均提高13.5%,而其硬件开销约为8.1%。     

一个关于程序时间性质的验证框架

运行时间是计算机程序的重要性质之一。对于运行时间而言,常用的时间复杂度分析技术基于的是抽象的算法,并非实际程序。而对于实际程序,大多数程序验证技术则不适合验证运行时间。提出一个运行时间的验证框架以解决这个问题,该框架适用于实际代码,而同时和复杂度分析一样,具有编程语言无关性。在对运行时间的性质要求较高的场合下,可以用于提高软件的可靠性。     

一个用于指针程序验证的自动定理证明器的设计与实现

对高可信软件需求的增加使得指针程序的验证成为近期的研究热点.指针逻辑作为Hoare逻辑的扩展,可以对指针程序进行精确的分析.介绍一个针对指针逻辑的自动定理证明器的设计和实现,描述了一些算法.实验结果表明,该定理证明器可以完全自动的证明用类C语言编写的关于单链表,双链表和二叉树的指针程序的验证条件,并生成机器可检查的证明.     

一种高效的集中信任模型下的共谋检测算法

在各种信任管理模型中,共谋欺骗是最棘手的恶意行为之一. 由于信任值的主观特性,目前对共谋欺骗还没有较好的判定方法. 本文利用聚类方法,提出一种集中信任模型下的共谋检测算法. 为检验算法性能和参数设置,文中设计了相关的仿真实验,并进行了量化分析. 实验结果表明,在选取合适参数的情况下,算法具有较好的检测效果.